The following papers provide useful background information, for which they are incorporated herein by reference in their entirety, and are selectively referred to in the remainder of this disclosure by their accompanying reference numbers in square brackets (i.e., [3] for the third numbered paper by Aspinall and Sevcik):
[1] S. V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, 1996; [2] L. Lamport. How to make multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers, 1979; [3] D. Aspinall and J. Sevcik. Formlising Java's data-race-free guarantee. Technical Report EDI-INF-RR-0958, School of Informatics, University of Edinburgh, 2007; [4] G. Ramalingam. Context sensitive synchronization sensitive analysis is undecidable. In ACM Transactions on Programming Languages and Systems, 2000; [5] P. Godefroid. Model checking for programming languages using verisoft. In Proc. ACM Symposium on Principles of Programming Languages, 1997; [6] T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. ZING: Exploiting program structure for model checking concurrent software. In Proc. of the Conference on Concurrency, 2004; [7] P. Godefroid. Partial-order Methods for the Verification of Concurrent Systems An Approach to the State-explosion Problem. PhD thesis, 1995; [8] C. Flanagan and S. Qadeer. Transactions for software model checking. In Proc. of TACAS, 2003; [9] S. D. Stoller. Model-checking multi-threaded distributed Java programs. International Journal on Software Tools for Technology Transfer, 2002; [10] S. D. Stoller and E. Cohen. Optimistic synchronization-based statespace reduction. In Proc. of TACAS, 2003; [11] V. Levin, R. Palmer, S. Qadeer, and S. K. Rajamani. Sound transaction-based reduction without cycle detection. In International SPIN Workshop on Model Checking of Software, 2003; [12] Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993; [13] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of TACAS, 1999; [14] M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a SAT solver. In Proc. of FMCAD, 2000; [15] R. Alur, R. K. Brayton, T. A. Henzinger, S. Qadeer, and S. K. Rajamani. Partial-order reduction in symbolic state space exploration. In Proc. of CAV, pages 340-351, 1997; [16] V. Kahlon, A. Gupta, and N. Sinha. Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In Proc. of CAV, 2006; [17] I. Rabinovitz and O. Grumberg. Bounded model checking of concurrent programs. In Proc. of CAV, 2005; [18] F. Lerda, N. Sinha, and M. Theobald. Symbolic model checking of software. In Electronic Notes Theoretical Computer Science, 2003; [19] S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In Proc. of TACAS, 2005; [20] B. Cook, D. Kroening, and N. Sharygina. Symbolic Model Checking for Asynchronous Boolean Programs. In International SPIN Workshop on Model Checking of Software, 2005; [21] O. Grumberg, F. Lerda, O. Strichman, and M. Theobald. Proof-guided Underapproximation-Widening for Multi-process Systems. In Proc. ACM Symposium on Principles of Programming Languages, 2005; [22] B. Dutertre and L. de Moura. A fast linear-arithmetic solver for DPLL(T). In Proc. of CAV, 2006; [23] R. Nieuwenhuis and A. Oliveras. DPLL(T) with exhaustive theory propagation and its application to difference logic. In Proc. of CAV, 2005; [24] C. Barrett, D. Dill, and Jeremy Levitt. Validity Checking for Combinations of Theories with Equality. In Proc. of FMCAD, November 1996; [25] M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. V. Rossum, M. Schulz, and R. Sebastiani. The MathSAT 3 system. In Proc. Of CADE, 2005; [26] M. K. Ganai and A. Gupta. Accelerating high-level bounded model checking. In Proc. Intl. Conf. on Computer-Aided Design, 2006; [27] S. V. Adve, M. D. Hill, B. P. Miller, and R. H. B. Netzer. Detecting data races on weak memory systems. In Proc. of ISCA, 1991; [28] Y. Yang, G. Gopalakrishnan, and G. Lindstrom. Memory-model sensitive data race analysis. In Proc. of SPIN Workshop, 2004; [29] S. Burckhardt, R. Alur, and M. M. K. Martin. CheckFence: Checking consistency of concurrent data types on relaxed memory models. In Proc. of Programming Language Design and Implementation, 2007; [30] Y. Yang, G. Gopalakrishnan, G. Lindstrom, and K. Slind. Nemos: A framework for axiomatic and executable specifications of memory consistency models. In Proc. of IPDPS, 2004; [31] L. Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978; [32] Joint CAV/ISSTA Special Event. Specification, Verification, and Testing of Concurrent Software. http://research.microsoft.com/quadeer/cavissta.htm, 2004; [33] L. de Moura, H. Rue_, and M. Sorea. Lazy theorem proving for bounded model checking over infinite domains. In Proc. of CADE, 2002.; [34] A. Armando, J. Mantovani, and L. Platania. Bounded Model Checking of Software Using SMT Solvers Instead of Sat Solvers. In International SPIN Workshop on Model Checking of Software, 2006; [35] M. K. Ganai, A. Gupta, and P. Ashar. Efficient modeling of embedded memories in bounded model checking. In Proc. of CAV, 2004.; [36] F. Ivancic, Z. Yang, M. K. Ganai, A. Gupta, I. Shlyakhter, and P. Ashar. F-soft: Software verification platform. In Proc. of CAV, 2005; [37] SRI Team. Yices: An SMT solver; [38] D. Kroening, E. Clarke, and K. Yorav. Behavioral consistency of c and verilog programs using bounded model checking. In Proc. of the Design Automation Conf., 2003.; and [39] F. Ivancic, Z. Yang, M. K. Ganai, A. Gupta, and P. Ashar. Efficient SAT-based Bounded Model Checking for Software Verification. In International Symposium for Leveraging Applications of Formal Methods, 2004.
The growth in number of inexpensive multi-processor systems and concurrent library support are making concurrent systems employing concurrent programming a very attractive approach for system designers. Unfortunately however, verification of concurrent systems remains a daunting task due in part to complex and unexpected interactions between asynchronous threads, and an assortment of architecture-specific memory consistency models [1] employed therein.
Various model checking efforts—both explicit and symbolic—for verifying concurrent systems having shared memory have been explored and described in the art. As known and described in the art, the general problem of verifying a concurrent system with even two threads with unbounded stacks is believed to be undecidable. Consequently, prior art verification efforts typically use incomplete methods or imprecise models—or sometimes both—to address the scalability of the problem.
Such prior art verification models are typically obtained by composing individual thread models using interleaving semantics, and model checkers are then applied to systematically explore the global state space. Well-known model checkers such as Verisoft and Zing explore states and transitions of the concurrent system using explicit enumeration. And while several state space reduction techniques based-on partial order methods and transactions-based methods have been proposed, these techniques do not scale well in general due to both state explosion and explicit enumeration.
As those skilled in the art will surely know, symbolic model checkers such as BDD-based SMV and SAT-based Bounded Model Checking (BMC) use symbolic representation and traversal of state space, and have been shown to be effective for verifying synchronous hardware designs. And while there have been efforts to combine symbolic model checking with the above mentioned state-reduction methods for verifying concurrent software, they unfortunately still suffer from a lack of scalability.
To overcome this limitation, some researchers have employed sound abstraction techniques with a bounded number of context switches while others have employed finite-state model abstractions with bounded depth analysis. These techniques may also be combined with a bounded number of context switches known a priori or a proof-guided method to discover them. Such efforts are generally geared toward state-reduction in the concurrent system model, and not toward size-reduction of the model checking instances.
Another development is the growing popularity of Satisfiability-Modulo Theory (SMT)-solvers. Due in-part to their support for richer expressive theories beyond Boolean logic coupled with several recent advancements, SMT-based methods are providing more scalable alternatives than BDD-based or SAT-based methods. Specifically, with several acceleration techniques, SMT-based BMC has been shown to scale better than SAT-based BMC for finding bugs. SMT-based BMC, therefore, is emerging as a potential replacement for SAT-based BMC for expressive models.
Simultaneously efforts have been made to detect bugs for weaker memory models. As is known a weak memory model increases the set of standard interleavings as it allows reordering of writes that may not follow program order, so as to capture the effect of write latency in an implemented memory architecture. Advantageously, one can check these models using axiomatic memory style specifications combined with constraint solvers. Note however that although these methods support various memory models they require a test program to address the scalability.